一階述語論理 (FOL)
first-order predicate logic (FOL)
命題論理 (殆どの場合は古典論理) に量化子$ \forall、$ \existを足したもの $ F\lbrack t/x\rbrackは、論理式$ Fでの變項$ xの全ての自由出現を、置き換へる事に依り新たに束縛される自由變項の無い (代入可能な (substitutable)) 別の項$ tに置き換へた論理式を表す
公理系
$ \forall x\phi\to\phi\lbrack t/x\rbrack普遍例化 (UI)
$ \forall x(\phi\to\psi)\to(\forall x\phi\to\forall x\psi)正規性
※$ tは任意の變項を表し、$ aは下式に現れない變項を表す事にする
論理規則
$ \forall(普遍汎化 (GEN)) :$ \frac{F\lbrack t/x\rbrack,\Gamma\vdash\Delta}{\forall xF,\Gamma\vdash\Delta}(\forall L),$ \frac{\Gamma\vdash\Delta,F\lbrack a/x\rbrack}{\Gamma\vdash\Delta,\forall xF}(\forall R)
$ \exist(存在汎化) :$ \frac{F\lbrack a/x\rbrack,\Gamma\vdash\Delta}{\exist xF,\Gamma\vdash\Delta}(\exist L),$ \frac{\Gamma\vdash\Delta,F\lbrack t/x\rbrack}{\Gamma\vdash\Delta,\exist xF}(\exist R)
汎化 / 例化
普遍汎化 (universal generalization。universal introduction。GEN)
$ \frac{\vdash F\lbrack t/x\rbrack}{\vdash\forall xF}論理式$ Fの自由變項$ xにどんな變項を代入してもよいなら$ xを全稱量化してよい
普遍例化 (universal instantiation。universal specification。universal elimination。UI)
$ \frac{\vdash\forall xF}{\vdash F\lbrack c/x\rbrack}論理式$ Fに現れる變項$ xを全稱量化してよいなら$ xに自由である定項を代入してよい
存在汎化 (existential generalization。existential introduction)
$ \frac{\vdash F\lbrack t/x\rbrack}{\vdash \exist xF}論理式$ Fの自由變項$ xにどんな變項を代入してもよいなら$ xを存在量化してよい
存在例化 (existential instantiation。existential elimination)
$ \frac{\vdash\exist xF}{\vdash F\lbrack c/x\rbrack}論理式$ Fに現れる變項$ xを存在量化してよいなら$ xに自由である定項を代入してよい
存在例化の誤謬
well-defined でない$ xに就いて$ \forall x~P(x)が言へても$ \exist x~P(x)は從はない
量化子 (限量子。quantifier)
全稱量化
略記$ \forall x_{\in A}Piff.$ \forall x(x\in A\supset P)
$ (\_\times Y\dashv\_^Y):{\bf C}\xrightleftarrows[\_\times Y]{\_^Y}{\bf C}
$ (x\in A\land P)\dashv(x\in A\supset P)?
存在量化
略記$ \exist x_{\in A}Piff.$ \exist x(x\in A\land P)
一意性$ \exist!
$ \exist!x.P(x)
$ \exist x(P(x)\land\forall y(P(x)\to x=y))
$ \exist x.P(x)\land\forall y,z((P(y)\land P(z))\to y=z)
$ \exist x\forall y(P(y)\lrarr x =y)
$ \Doteqwell-defined
guard 附き量化
議論領域を指定する
量化子消去 (quantifier elimination)
擴張
動的述語論理 (dynamic predicate logic)
一般量化子